FDL - Nuprl Definition : existse-before

Nuprl Definition : existse-before

11,40

e<e'.P(e) ==

e:es-E(es). (es-locl(es; e; e') c

P(e))

clarification:

existse-before(es;e';e.P(e)) ==

e:es-E(es). (es-locl(es; e; e') c

P(e))

Definitions x:A. B(x), es-E(es), A c B, es-locl(es; e; e')

FDL editor aliases existse-before

Definitions	x:A. B(x), es-E(es), A c B, es-locl(es; e; e')
FDL editor aliases	existse-before